Deterministic timed automata are strictly less expressive than theirnon-deterministic counterparts, which are again less expressive than those withsilent transitions. As a consequence, timed automata are in generalnon-determinizable. This is unfortunate since deterministic automata play amajor role in model-based testing, observability and implementability. However,by bounding the length of the traces in the automaton, effectivedeterminization becomes possible. We propose a novel procedure for boundeddeterminization of timed automata. The procedure unfolds the automata tobounded trees, removes all silent transitions and determinizes via disjunctionof guards. The proposed algorithms are optimized to the bounded setting andthus are more efficient and can handle a larger class of timed automata thanthe general algorithms. The approach is implemented in a prototype tool andevaluated on several examples. To our best knowledge, this is the firstimplementation of this type of procedure for timed automata.
展开▼
